Inference at * 2 2 
Iof proof for Lemma before-adjacent:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x, y:T.
5. no_repeats(T;v)  adjacent(T;v;x;y)  (z:T. z before y  v  (z before x  v  (z = x)))
6. x : T
7. y : T
8. no_repeats(T;[u / v])
9. 0 < ||v||
10. adjacent(T;v;x;y)
11. z : T
12. z before y  [u / v]
  z before x  [u / v]  (z = x) 

latex

 by ((((RWO "no_repeats_cons" (-5)) 
CollapseTHEN (Auto))) 
CollapseTHEN (((InstHyp [x;y] 5) 

CoCollapseTHEN (Auto)))) 

latex

C1: 

C1: 8. no_repeats(T;v)
C1: 9. (u  v)
C1: 10. 0 < ||v||
C1: 11. adjacent(T;v;x;y)
C1: 12. z : T
C1: 13. z before y  [u / v]
C1: 14. z:T. z before y  v  (z before x  v  (z = x))
C1:   z before x  [u / v]  (z = x)
C.

Definitions	P  Q, P & Q, x:A  B(x), P  Q, t  T, adjacent(T;L;x;y), a < b, A, no_repeats(T;l), type List, Type, x before y  l, s = t, ||as||, x:A. B(x), x:AB(x), P  Q, left + right
Lemmas	no repeats cons, l before wf